Crate isotope[][src]

Expand description

The Isotope Project

isotope is an experimental dependently typed language supporting borrow checking, designed for use as an intermediate representation for building verifiable systems languages.

isotope is composed of two languages: the “main” or “implementation” language, and a “term” language. Expressions in the “main” language describe dependently typed RVSDGs extended with lifetimes, which are given denotations in the “term” language, which ignores low-level details such as lifetimes and representation. In turn, the types of these expressions may depend only on values in the “term” language, with programs, representations, and “main” language types themselves values like any other. The “term” language itself is a simplified implementation of the Calculus of Constructions, inspired by Lean, extended with Zombie-like support for congruence-based normalization.

Re-exports

pub use error::Error;

Modules

ast

Convert isotope terms to abstract syntax trees

builder

Convert isotope ASTs to terms

ctx

Contexts for creating, normalizing, and type-checking isotope terms

error

Error handling utilities

prelude

Commonly used items

primitive

Primitive isotope values

program

isotope program graphs

repr

Machine representations for isotope values and types

term

Terms in isotope’s underlying dependent type system

typing

Datatypes for isotope values

utils

Utilities

Macros

for_annot_ref

Return the same expression for every variant of Annotation

for_term

Return the same expression for every variant of Term